a:, b:. |a rem b| < |b| 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), P  Q, P & Q, , P  Q, P  Q, True, T, False, a  b  T , A, , P  Q, Dec(P), , A  B, , S  T
Lemmas	int nzero wf, nat plus wf, decidable le, rem bounds 1, nat plus inc, le wf, remainder wf, absval pos, nat plus inc int nzero, rem antisym, true wf, squash wf, nat wf, absval wf, absval sym, rem sym